1. Technical Field
The present invention relates to solving non-linear real decision problems, and more particularly, to a solver which separately handles Boolean, linear and non-linear solving phases.
2. Description of the Related Art
Modern program analysis and verification tools include solvers which are used for Satisfiability Modulo Theories (SMT) problems. While SMT solvers have been improved in recent years for linear problems, there has been little progress with respect to providing a sufficient SMT solver for non-linear real problems, particularly with respect to quantifier-free non-linear (QFNR) decision problems. Consequently, there is no generally accepted design for solvers handling QFNR or non-linear problems, and these types of problems still present major difficulties in nearly all domains.
A major problem associated with conventional solvers relates to the fact that they handle linear and non-linear constraints in the same or similar manner. In doing so, conventional solvers neglect the fact that linear constraints can be handled differently from non-linear constraints in manner that is more complete, accurate, and efficient.